Left Termination of the query pattern
gtsolve(g,a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

gtsolve(X, Y) :- ','(generate(X, Y), test(Y)).

Query: gtsolve(g,a)

(1) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(2) Obligation:

Clauses:

gtsolve(X, Y) :- ','(generate(X, Y), test(Y)).
generate(X0, X1).
test(X0).

Query: gtsolve(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
gtsolve_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

gtsolve_in_ga(X, Y) → U1_ga(X, Y, generate_in_ga(X, Y))
generate_in_ga(X0, X1) → generate_out_ga(X0, X1)
U1_ga(X, Y, generate_out_ga(X, Y)) → U2_ga(X, Y, test_in_a(Y))
test_in_a(X0) → test_out_a(X0)
U2_ga(X, Y, test_out_a(Y)) → gtsolve_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
gtsolve_in_ga(x1, x2)  =  gtsolve_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
generate_in_ga(x1, x2)  =  generate_in_ga(x1)
generate_out_ga(x1, x2)  =  generate_out_ga
U2_ga(x1, x2, x3)  =  U2_ga(x3)
test_in_a(x1)  =  test_in_a
test_out_a(x1)  =  test_out_a
gtsolve_out_ga(x1, x2)  =  gtsolve_out_ga

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

gtsolve_in_ga(X, Y) → U1_ga(X, Y, generate_in_ga(X, Y))
generate_in_ga(X0, X1) → generate_out_ga(X0, X1)
U1_ga(X, Y, generate_out_ga(X, Y)) → U2_ga(X, Y, test_in_a(Y))
test_in_a(X0) → test_out_a(X0)
U2_ga(X, Y, test_out_a(Y)) → gtsolve_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
gtsolve_in_ga(x1, x2)  =  gtsolve_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
generate_in_ga(x1, x2)  =  generate_in_ga(x1)
generate_out_ga(x1, x2)  =  generate_out_ga
U2_ga(x1, x2, x3)  =  U2_ga(x3)
test_in_a(x1)  =  test_in_a
test_out_a(x1)  =  test_out_a
gtsolve_out_ga(x1, x2)  =  gtsolve_out_ga

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

GTSOLVE_IN_GA(X, Y) → U1_GA(X, Y, generate_in_ga(X, Y))
GTSOLVE_IN_GA(X, Y) → GENERATE_IN_GA(X, Y)
U1_GA(X, Y, generate_out_ga(X, Y)) → U2_GA(X, Y, test_in_a(Y))
U1_GA(X, Y, generate_out_ga(X, Y)) → TEST_IN_A(Y)

The TRS R consists of the following rules:

gtsolve_in_ga(X, Y) → U1_ga(X, Y, generate_in_ga(X, Y))
generate_in_ga(X0, X1) → generate_out_ga(X0, X1)
U1_ga(X, Y, generate_out_ga(X, Y)) → U2_ga(X, Y, test_in_a(Y))
test_in_a(X0) → test_out_a(X0)
U2_ga(X, Y, test_out_a(Y)) → gtsolve_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
gtsolve_in_ga(x1, x2)  =  gtsolve_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
generate_in_ga(x1, x2)  =  generate_in_ga(x1)
generate_out_ga(x1, x2)  =  generate_out_ga
U2_ga(x1, x2, x3)  =  U2_ga(x3)
test_in_a(x1)  =  test_in_a
test_out_a(x1)  =  test_out_a
gtsolve_out_ga(x1, x2)  =  gtsolve_out_ga
GTSOLVE_IN_GA(x1, x2)  =  GTSOLVE_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
GENERATE_IN_GA(x1, x2)  =  GENERATE_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
TEST_IN_A(x1)  =  TEST_IN_A

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GTSOLVE_IN_GA(X, Y) → U1_GA(X, Y, generate_in_ga(X, Y))
GTSOLVE_IN_GA(X, Y) → GENERATE_IN_GA(X, Y)
U1_GA(X, Y, generate_out_ga(X, Y)) → U2_GA(X, Y, test_in_a(Y))
U1_GA(X, Y, generate_out_ga(X, Y)) → TEST_IN_A(Y)

The TRS R consists of the following rules:

gtsolve_in_ga(X, Y) → U1_ga(X, Y, generate_in_ga(X, Y))
generate_in_ga(X0, X1) → generate_out_ga(X0, X1)
U1_ga(X, Y, generate_out_ga(X, Y)) → U2_ga(X, Y, test_in_a(Y))
test_in_a(X0) → test_out_a(X0)
U2_ga(X, Y, test_out_a(Y)) → gtsolve_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
gtsolve_in_ga(x1, x2)  =  gtsolve_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
generate_in_ga(x1, x2)  =  generate_in_ga(x1)
generate_out_ga(x1, x2)  =  generate_out_ga
U2_ga(x1, x2, x3)  =  U2_ga(x3)
test_in_a(x1)  =  test_in_a
test_out_a(x1)  =  test_out_a
gtsolve_out_ga(x1, x2)  =  gtsolve_out_ga
GTSOLVE_IN_GA(x1, x2)  =  GTSOLVE_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
GENERATE_IN_GA(x1, x2)  =  GENERATE_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
TEST_IN_A(x1)  =  TEST_IN_A

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 4 less nodes.

(8) TRUE